/* exercice 2 */

    partition_positifs([],[],[]).
    partition_positifs([X|L],[X|R],S):-X>0,!,partition_positifs(L,R,S).
    partition_positifs([X|L],R,[X|S]):-partition_positifs(L,R,S).

    partition([],_,[],[]).
    partition([X|L],P,[X|R],S):-Q=..[P,X],Q,!, partition(L,P,R,S).
    partition([X|L],P,R,[X|S]):-partition(L,P,R,S).

/* exercice 3 */

    est_cnf([]).
    est_cnf([X|L]):-est_clause(X), est_cnf(L).

    est_clause([]).
    est_clause([X|L]):-est_litteral(X),est_clause(L).

	       est_litteral(X):-atomic(X); (X=neg(Y), atomic(Y)).


    redondant(C):-member(X,C),member(Y,C),Y=neg(X).
    normalise([],[]).
    normalise([X|L],R):-redondant(X),!,normalise(L,R). 
    normalise([X|L],[X|R]):-normalise(L,R).

/* ...tres vite fait a partir de la*/
    
    retire([X|L],X,L):-!.
    retire([Y|L],X,[Y|G]):-retire(L,X,G).

    evalue([],_,[]).
    evalue([C|L],(X,B),G):- (B=1,member(X,C)),!, evalue(L,(X,B), G).
    evalue([C|L],(X,B),G):- (B=0,member(neg(X),C)),!, evalue(L,(X,B), G).
    evalue([C|L],(X,B),[C1|G]):- (B=0,member(X,C)),!, 
    retire(C,X,C1), evalue(L,(X,B), G).
    evalue([C|L],(X,B),[C1|G]):- (B=1,member(neg(X),C)),!, 
    retire(C,neg(X),C1), evalue(L,(X,B), G).
    evalue([C|L],(X,B),[C|G]):-evalue(L,(X,B), G).

choosevar([C|_],X):-member(Y,C), (atomic(Y) -> X=Y; Y=neg(X)).
choosevar([_|L],X):-choosevar(L,X).



dpll([],R,R):-!.
dpll(F,L,R):-choosevar(F,X),evalue(F,(X,1),F1), 
dpll(F1,[(X,1)|L],R),!.

   dpll(F,L,R):-choosevar(F,X),evalue(F,(X,0),F1), 
dpll(F1,[(X,0)|L],R),!.

affectations(F,L):-dpll(F,[],L).

/* exercice 4 */

    move(N,M):- (N>1,M is N-2);(N>2,M is N-3).
    gagne(N):-move(N,M),not(gagne(M)).

    gagne1(N):- P is (N mod 5), (P=\=0;P=\=1).